/*
 * VariableSetting.hpp
 *
 * Copyright 2012 Fabian Wenzelmann
 *
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 *
 * Recognition-Procedures-for-Boolean-Functions is free software: you
 * can redistribute it and/or modify it under the terms of the
 * GNU General Public License as published by the Free Software Foundation,
 * either version 3 of the License, or (at your option) any later version.
 *
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope
 * that it will be useful, but WITHOUT ANY WARRANTY; without even the implied
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General
 * Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.
 *
 * If not, see <http://www.gnu.org/licenses/>.
 */

#ifndef VARIABLESETTING_HPP_
#define VARIABLESETTING_HPP_

#include <vector>

#include "bfr/OccurrencePattern.hpp"
#include "bfr/ClauseSet.hpp"

namespace bfr {

/**
 * This class is used to store global information about all variables.
 *
 * It can be created given a DNF and an occurrence pattern factory.
 * It will <b>sort</b> the variables according the \f$\succeq\f$ ordering.
 *
 * Then you can ask which variable is on position <i>i</i> in the global
 * ordering (#getPos). You can also ask what is the position of variable
 * <i>v</i> in the global ordering (#operator[]).
 */
class VariableSetting {

	public:
                /**
                 * Constructor.
                 *
                 * Create a variable setting given a DNF and an
                 * occurrence pattern factory.
                 *
                 * It will create the occurrence patterns for the DNF
                 * and sort them according to the \f$\succeq\f$ ordering.
                 */
		VariableSetting(const ClauseSet *dnf);

		/**
		 * Destructor.
		 *
		 * Does nothing.
		 */
		~VariableSetting();

		/**
		 * Return the ordered sequence of the occurrence patterns.
		 *
		 * This are the occurrence patterns for the initial DNF.
		 *
		 * @return The ordered sequence of the occurrence patterns.
		 */
		std::vector<OccurrencePattern*> *getOrderedPatterns();

		/**
		 * Returns the variable id of the variable in position
		 * <code>index</code> in the global ordering.
		 *
		 * @param index The position in the global ordering.
		 *
		 * @return variable id of the variable in position
                 * <code>index</code> in the global ordering.
		 */
		size_t operator[](const size_t index) const;

		/**
		 * Return the position of the variable with
		 * id <code>variableID</code> in the global ordering.
		 *
		 * @param variableID Id of the variable.
		 *
		 * @return The position of the variable with
                 * id <code>variableID</code> in the global ordering.
		 */
		size_t getPos(const size_t variableID) const;

		/**
		 * Return the size of this variable setting.
		 *
		 * The size is the number of variables in the
		 * initial DNF.
		 *
		 * @return Number of variables in the initial DNF.
		 */
		size_t size() const;

	private:
		void init(const ClauseSet *dnf);
		std::vector<OccurrencePattern*> *occurrences;
		std::vector<size_t> variablePos;

};

}

#endif  // VARIABLESETTING_HPP_
